E:Type, V:(KndIdType), info:(E((:Id  Id) + (:(:IdLnk  E)  Id))), val:(e:EV
E:Type, V:(KndIdType), info:(E((:Id  Id) + (:(:IdLnk  E)  Id))), val:(e:E(kind(e)
E:Type, V:(KndIdType), info:(E((:Id  Id) + (:(:IdLnk  E)  Id))), val:(e:E,loc(e))),
e:E. (rcv?(e))  (rmsg(info; val; e)  Msg(l,tg. V(rcv(l,tg),destination(l)))) 

latex

Definitions	x:A. B(x), kind(e), loc(e), P  Q, b, rcv?(e), t  T, rmsg(info; val; e), link(e), rtag(info; e), t.2, t.1, ecase1(e;info;i.f(i);l,e'.g(l;e')), ff, tt, if b then t else f fi , False, prop{i:l}
Lemmas	kind wf, loc wf, IdLnk wf, false wf, locl wf, msg wf, rcv wf, ldst wf, true wf, assert wf, rcv? wf, Id wf, Knd wf